ds:fpf(Id; x.Type), da:fpf(Knd; k.Type), A:ecl-trans-tuple{i:l}
ds:fpf(Id; x.Type), da:fpf(Knd; k.Type), A:ecl-trans-tuple(ds; da).
ecl-trans-a(A)
 (k:{k:Knd| (k  ecl-trans-ks(A))} decl-state(ds)ma-valtype(da; k)ecl-trans-type(A)
 () 

latex

Definitions	t  T, spreadn(u; a,b,c,d,e,f,g.v(a;b;c;d;e;f;g)), ecl-trans-a(v), ecl-trans-type(A), ecl-trans-ks(v), ecl-trans-tuple{i:l}(ds; da), Id, x. t(x), x:A. B(x), fpf(A; a.B(a)), Knd, , (x  l), decl-state(ds), ma-valtype(da; k),
Lemmas	ecl-trans-tuple wf, Knd wf, fpf wf, Id wf